Step of Proof: add_functionality_wrt_le 12,41
Inference at * 1 
Iof proof for Lemma add functionality wrt le:



1. i1 : 
2. i2 : 
3. j1 : 
4. j2 : 
5. i1  j1
6. i2  j2
  (i1+i2)  (j1+j2) 
latex
 by MoveToConcl 3 
latex

 1: 

 1: 3. j2 : 
 1: 4. i2  j2
 1:   j1:. (i1  j1)  ((i1+i2)  (j1+j2))
 .

Definitionst  T, x:A. B(x), P  Q

origin